$\forall$$T$:Type, $R$:($T$$\rightarrow$$T$$\rightarrow$Prop), $n$:$\mathbb{N}$, $x$, $y$:$T$. ($x$ $R$\^{}$n$$^{\mbox{\scriptsize {-}1}}$ $y$) $\Leftrightarrow$ ($x$ $R$$^{\mbox{\scriptsize {-}1}}$\^{}$n$ $y$)